(* # ===================================================================
   # Matrix Project
   # Copyright FEM-NUAA.CN 2020
   # =================================================================== *)


 (** ** Complex MMatrix Module *)
From Coquelicot Require Import Complex.
Require Import Reals.
Open Scope R_scope.
Require Export Matrix.MMat.MMatrix_Module.
Require Export Matrix.Mat.CMatrix.

Module CMMatrix := MMatrix CM.

Definition CMMO := CMMatrix.MMO.

Definition CMMI := CMMatrix.MMI.

Definition CMMeq := @CMMatrix.MMeq.
Arguments CMMeq {m}{n}{m2}{n2}.

Definition CMMadd := @CMMatrix.MMadd.
Arguments CMMadd {m0}{n0}{m}{n}.

Definition CMMopp := @CMMatrix.MMopp.
Arguments CMMopp {m0}{n0}{m}{n}.

Definition CMMsub := @CMMatrix.MMsub.
Arguments CMMsub {m0}{n0}{m}{n}.

Definition CMMmult := @CMMatrix.MMmult.
Arguments CMMmult {m}{n}{p}{m2} {n2} {p2}.

Definition CMMadd_comm:=@CMMatrix.MMadd_comm.
Definition CMMadd_assoc:=@CMMatrix.MMadd_assoc.
Definition CMMadd_zero_l:=@CMMatrix.MMadd_zero_l.
Definition CMMadd_zero_r:=@CMMatrix.MMadd_zero_r.

Definition CMMsub_opp:=@CMMatrix.MMsub_opp.
Definition CMMsub_assoc:=@CMMatrix.MMsub_assoc.
Definition CMMsub_zero_l:=@CMMatrix.MMsub_zero_l.
Definition CMMsub_zero_r:=@CMMatrix.MMsub_zero_r.
Definition CMMsub_self:=@CMMatrix.MMsub_self.

Definition CMMmul_add_distr_l:= @CMMatrix.MMmul_add_distr_l.
Definition CMMmul_add_distr_r:= @CMMatrix.MMmul_add_distr_r.
Definition CMMmul_sub_distr_l:= @CMMatrix.MMmul_sub_distr_l.
Definition CMMmul_sub_distr_r:= @CMMatrix.MMmul_sub_distr_r.
Definition CMMmul_assoc:= @CMMatrix.MMmul_assoc.
Definition CMMmul_zero_l := @CMMatrix.MMmul_zero_l.
Definition CMMmul_zero_r := @CMMatrix.MMmul_zero_r.

Definition CMMtteq:= @CMMatrix.MMtteq.
Definition CMMtrans_add:= @CMMatrix.MMtrans_add.
Definition CMMtrans_sub:= @CMMatrix.MMtrans_sub.
Definition CMMtrans_mul:= @CMMatrix.MMtrans_mul.




